$\forall$$x$:chain\_config(). ($\uparrow$ccsucc?($x$)) $\Rightarrow$ (ccsucc{-}id($x$) $\in$ Id)